\chapter{Sorting an array}

\begin{quest}
	Determine the smallest integer $k$, for which the algorithm
	\begin{verbatim}
	    for j := 1 to k:
	       for i := 1 to  6: sort(i, 13-i)
	       for i := 1 to 11: sort(i,  1+i)
	\end{verbatim}
	is the correct sorting routine for all $12$-element arrays.
\end{quest}

Obviously, the task is, given a number $k$, to find a twelve-element array for which this routine
does not yield a sorted result. If $k$ is high enough, this requirement will be unsatisfiable.
If $k$ is low enough, we should get a satisfying valuation: the array that gets sorted incorrectly.

\section{SMT solver and encoding} For this task, we used the \textsc{Yices} SMT solver since
we are dealing with numbers.\footnote{In fact, we also tried \textsc{bddsolve} but that ended up
badly.} We represented the problem using three matrices of type $(k+1) \times 12$, named $S$, $M$,
and $N$. For example, the master matrix $S = \{s_{ji}\}$ looks like this (we use zero-based indices):

\[
\xymatrix@=0mm{
  \ar@{-->}[ddddd]_{\text{iteration}} \ar@{-->}[rrrrr]^{\text{array index}} & & & & &  \\
	& s_{0,0} & s_{0,1} & s_{0,2} & \cdots & s_{0,11} \\
	& s_{1,0} & s_{1,1} & s_{1,2} & \cdots & s_{1,11} \\
	& s_{2,0} & s_{2,1} & s_{2,2} & \cdots & s_{2,11} \\
	&         & \vdots  &         & \ddots & \vdots  \\
	& s_{k,0} & s_{k,1} & s_{k,2} & \cdots & s_{k,11}
}
\]
\vspace{2mm}

\noindent The $j$-th row of the matrix $S$ represents the state of the array after $j$ iterations.

Besides $S$, we have also two other matrices in our representation, called $M$ and $N$, with exactly
the same shape as $S$.\footnote{Last rows of these two matrices are actually unused but we don't bother
with this fact for simplicity.} This is because in each iteration, we need two intermediate arrays to
calculate the next row of the master matrix. This dependency can be seen in
Figure \ref{fig:datadeps} on page \pageref{fig:datadeps} and will be made clear in the following
subsections.

\section{Initial and final condition}

Given a value of $k$, we can express the initial and final condition as follows. Recall that the row
$s_0$ represents the input array, $s_k$ represents the output of the sorting algorithm.

\subsection{Initial condition}

Instead of considering all possible values of the elements of the input array (the elements are not
constrained by the assignment in any way so we cannot make any assumptions about them), we will operate
only with $s_{0,i} \in \{0,1,\ldots,11\}$; $s_{0,i} \neq s_{0,j\neq i}$. We won't go into
all gory details but it is probably obvious that any permutation of $[0,1,\ldots,11]$ can be sorted
in $k$ steps if and only if any array of size $12$ can be sorted in $k$ steps --- hence we can
consider only permutations of $[0,1,\ldots,11]$ as input arrays.

Hence our initial condition is as follows:
\begin{equation}
\begin{split}
	\mathsf{initial}(s_0) &=
		\bigwedge_{0 \leq i \leq 11}  \; (s_{0,i} < 12) \wedge (s_{0,i} \geq 0) \\
		& \quad \wedge \; \bigwedge_{i < j}  \; s_{0,i} \neq s_{0,j}
\end{split}
\end{equation}

\subsection{Final condition}

We want our array to remain unsorted, even after $k$ steps. If the array is unsorted, we can certainly
find a pair $s_{k,i} > s_{k,i+1}$. Hence the final condition is:
\begin{equation}
	\mathsf{final}(s_k) = \bigvee_{0 \leq i < 11} \; s_{k,i} > s_{k,i+1}
\end{equation}

\section{Transition}

Each transition corresponds to a (top-most) iteration of the sorting algorithm: it calculates the next
row of the matrix $S$ from the previous one.

\textit{Technical note.} A transition always occurs between two states. In the following text,
we will implicitly assume that we are considering transition from the state number $j$ to the state
number $j+1$.

However, the top-most iteration gets quite involved inside: we need to do 6 steps in the first subloop,
followed by 11 steps in the second subloop. If we modelled each intermediate state as a row in the
matrix $S$, the number of variables would blow up infeasibly. Therefore, we need to find a smarter way
to perform the substeps, namely, we will combine each subloop in a single operation.

We combine the first subloop into a single step called \emph{halfsort}, which, given $s_j$, yields
an auxiliary array $m_j$, that is actually the state of the master array after halfsorting.

Then, we calculate running maximum of $m_j$, which we name $n_j$, and using this additional array,
we can calculate the next state of the master array $s_{j+1}$ in parallel, too.

The whole diagram can be seen in Figure \ref{fig:datadeps} and now we are  going to discuss the details
of the operations shown in the diagram.

\begin{figure}[ht]
\[\xymatrixcolsep{15mm} \xymatrix{
	 s_j  \ar[r]^{\text{halfsort}}
	 	& m_j \ar[r]^{\text{running max}} \ar[rd]
	 	& n_j \ar[d] \\
	 & & s_{j+1}
}\]
\caption{Data dependencies of a single iteration}
\label{fig:datadeps}
\end{figure}


\subsection{Halfsort}

We named the first subloop (Figure \ref{fig:halfsort}) \emph{halfsort} because it divides the array in
halves and then sorts the corresponding elements.

\begin{figure}[htp]
	\centering
	\verb!for i := 1 to 6 do sort(i, 13-i)!
	\caption{Halfsort}
	\label{fig:halfsort}
\end{figure}

This operation is very parallelization-friendly (Figure \ref{fig:hsort-par}) and we can do it in one
step because there are no data dependencies between iterations of the loop over $i$.

\begin{figure}[htp]
	\centering
	\begin{tikzpicture}[x=5mm,y=5mm]
		\draw[step=1] (-6,0) grid (6,1);
		\draw[<->] (-5.5,-0.1) .. controls (-5.5,-3) and (5.5,-3) .. (5.5,-0.1);
		\draw[<->] (-4.5,-0.1) .. controls (-4.5,-2.2) and (4.5,-2.2) .. (4.5,-0.1);
		\draw[<->] (-0.5,-0.1) .. controls (-0.5,-1) and (0.5,-1) .. (0.5,-0.1);
		\draw (0,-1.1) node{$\vdots$};
	\end{tikzpicture}
	\caption{Halfsort can be parallelized easily}
	\label{fig:hsort-par}
\end{figure}

Hence, using the following formula, we calculate the first auxiliary array, $m_j$ from the current
master array $s_j$, in parallel, without going through multiple intermediate states (unlike the
imperative program).

\begin{equation}
	\mathsf{halfsort}(s_j, m_j) = \bigwedge_{0 \leq i \leq 5} \; \mathsf{sort}(i, 11-i, s_j, m_j)
\end{equation}
Now we have arrived at the need to define the \textsf{sort} predicate (note that $x$ and $y$
are \emph{rows} of matrices):
\begin{equation}
\begin{split}
	\mathsf{sort}(k,l,x,y) ={} &
		\mathsf{if} \; (k < l) \;\mathsf{xor}\; (x_k < x_l) \\
		& \quad\mathsf{then}\; (y_k = x_l \wedge y_l = x_k) \\
		& \quad\mathsf{else}\; (y_k = x_k \wedge y_l = x_l) \mint{,}
\end{split}
\end{equation}
which concludes the definition of \emph{halfsort}.\footnote{In our program, the condition
$k < l$ always holds and we use a slightly different definition, without the \textsf{xor}.}

\subsection{Pairsort}

We named the other subloop --- somewhat imprecisely --- \emph{pairsort}, since it traverses adjacent
pairs and sorts them (Figure \ref{fig:pairsort}).

\begin{figure}[htp]
	\centering
	\verb!for i := 1 to 11 do sort(i, i+1)!
	\caption{Pairsort}
	\label{fig:pairsort}
\end{figure}

Now, we don't see directly that this calculation can be parallelized because there are long chains
of data dependencies and, in the worst case, the leftmost element can ,,bubble-travel'' all the way
to the right (Figure  \ref{fig:pairsort-deps}).

\begin{figure}[htp]
	\centering
	\begin{tikzpicture}[x=5mm,y=5mm]
		\draw[step=1] (-6,0) grid +(12,1);
		\draw[step=1] (-6,-4) grid +(12,1);
		\foreach \i in {0,...,4} {
			\draw[<->] (-5.5+\i,-0.1-0.3*\i)
				.. controls +(0,-0.5) and +(0,-0.5)
				.. +(1,0);
			\draw[dotted] (-4.5+\i,-0.1) -- +(0,-0.3*\i);
			\draw[dotted,->] (-5+\i,-0.6-0.3*\i) -- (-5.5+\i,-2.9);
		}
		\draw (0.5,-1.7) node{$\cdots$};
	\end{tikzpicture}
	\caption{Pairsort and data dependencies}
	\label{fig:pairsort-deps}
\end{figure}

However, we can make the following observation:
\begin{align}
	\mathsf{pairsort}(x)_i = \min \left( \max_{j \leq i} x_j, \, x_{i+1} \right) \mint{,}
\end{align}
with the exception of the rightmost element, where $\mathsf{pairsort}(x)_{i_{max}} = \max x_j$.

This gives us the opportunity to calculate an intermediate array of running maxima and then use
that (and the original array) to calculate the final pairsorted array. Let us call the array
of running maxima $n_j$. Then the predicates describing relations between $m_j$, $n_j$ and the
final array state $s_{j+1}$ are as follows.
\begin{align}
	\mathsf{pairsort}(m_j, n_j, s_{j+1}) &=
		\mathsf{running\_max}(m_j, n_j)
		\wedge \mathsf{merge}(m_j, n_j, s_{j+1}) \mint{,} \\
\intertext{with the following subpredicates:}
	\begin{split}
	\mathsf{running\_max}(m_j, n_j) &= (n_{j0} = m_{j0}) \\
		&\quad \wedge \bigwedge_{0 < i \leq 11}
		\mathsf{if}\;(m_{ji} > n_{j,i-1})
			\;\mathsf{then}\;(n_{ji} = m_{ji})
			\;\mathsf{else}\;(n_{ji} = n_{j,i-1})
	\end{split} \\
	\begin{split}
	\mathsf{merge}(m_j, n_j, s_{j+1}) &= (s_{j+1,11} = n_{j,11}) \\
		&\quad \wedge \bigwedge_{0 \leq i < 11}
		\mathsf{if}\;(n_{ji} < m_{j,i+1})
			\;\mathsf{then}\;(s_{j+1,i} = n_{ji})
			\;\mathsf{else}\;(s_{j+1,i} = m_{j,i+1})
	\end{split}
\end{align}

\subsection{Transition, combined}

By combining the previous two relations, we get the transition relation:
\begin{equation}
	\mathsf{trans}(s_j, m_j, n_j, s_{j+1}) =
		\mathsf{halfsort}(s_j, m_j)	\wedge \mathsf{pairsort}(m_j, n_j, s_{j+1})
\end{equation}

\section{Putting it all together}

Now we have everything ready to plug into the final formula. Suppose we choose the number of
iterations $k$. Then the following formula describes the sorting procedure, along with its initial and
final constraints, that is, describes an \emph{incorrect} sorting procedure. The algorithm is then 
correct for the given $k$ if and only if this formula is unsatisfiable.
\begin{align*}
	\mathsf{sorted}(S,M,N)
		&= \mathsf{initial}(s_0) 
			\wedge \left[ \bigwedge_{0 \leq j < k} \mathsf{trans}(s_j, m_j, n_j, s_{j+1}) \right]
			\wedge \mathsf{final}(s_k)
\end{align*}

\subsection{Implementation and code}
For concise notation of all formulas, we used a \textsc{Haskell} embedded DSL that generates
\textsc{Yices} formulas from higher-order input.\footnote{
The resulting program is available at \url{http://code.google.com/p/reasoning-homework/source/browse/trunk/sorting.hs}.
}

\subsection{Solution}

\begin{itemize}
	\item For $k = 6$, after roughly $30$ seconds, the \textsc{Yices} program outputs the resolution
			\emph{unsatisfiable}.
	\item For $k = 5$, the program finds the following incorrectly sorted input:
	\[
		\begin{array}{rrrrrrrrrrrrr}
		\text{input:} &  5 & 1 & 6 &10 & 7 &11 & 3 & 8 & 2 & 9 & 0 & 4 \\
		1: &  0 & 4 & 2 & 6 & 3 & 7 & 8 &10 & 9 & 1 & 5 &11 \\
		2: &  0 & 1 & 4 & 3 & 6 & 7 & 8 & 9 & 2 & 5 &10 &11 \\
		3: &  0 & 1 & 2 & 4 & 6 & 7 & 8 & 3 & 5 & 9 &10 &11 \\
		4: &  0 & 1 & 2 & 3 & 4 & 7 & 6 & 5 & 8 & 9 &10 &11 \\
		\text{output}: &  0 & 1 & 2 & 3 & 4 & \mathbf{6} & \mathbf{5} & 7 & 8 & 9 &10 &11
		\end{array}
	\]
\end{itemize}

\subsection{Remarks}

Although we described the solution here assuming that the length of the array to be sorted is $12$,
it is trivial to extend the solution to work with any array length --- which we actually do in
the \textsc{Haskell} program.




































































